Nuprl Lemma : l_member_set
0,22
postcript
pdf
A
:Type,
P
:(
A
Prop),
L
:
A
List,
x
:
A
. (
x
L
.
P
(
x
))
{(
x
L
)
(
x
L
)}
latex
Definitions
x
(
s
)
,
{
T
}
,
x
.
t
(
x
)
,
x
L
.
P
(
x
)
,
(
x
l
)
,
x
:
A
.
B
(
x
)
,
l
[
i
]
,
i
j
,
A
&
B
,
S
T
,
x
:
A
.
B
(
x
)
,
,
A
B
,
A
,
False
,
P
Q
,
||
as
||
,
t
T
,
Prop
Lemmas
list-set-type2
,
select
wf
,
length
wf1
,
l
all
wf
,
l
member
wf
origin
A:Type, P:(A
Prop), L:A List, x:A. (x
L. P(x)) 
{(x L) (x L)} A:Type, P:(AProp), L:A List, x:A. (xL. P(x)) {(x L) (x L)} 
x. t(x)xL. P(x) l)
x:A. B(x)
j
Tx:A. B(x)
B
A Q T